Inductive BoolExp : Type := 
  | bool_exp_lit : Bool     -> BoolExp
  | bool_exp_id  : Id       -> BoolExp
  | bool_exp_eq  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_lt  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_le  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_gt  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_gtb : ByteExp  -> ByteExp  -> BoolExp
  | bool_exp_eqb : ByteExp  -> ByteExp  -> BoolExp
  | bool_exp_ge  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_not : BoolExp  -> BoolExp
  | bool_exp_and : BoolExp  -> BoolExp  -> BoolExp
  | bool_exp_or  : BoolExp  -> BoolExp  -> BoolExp
.